ngying(** ** M_FST:*)(*初等矩阵*)

Require Export List.
Require Export Matrix.list_function.
Require Export Matrix.Mat_def.

Section Matrix_FST.

Variable A:Set.
Variable Zero:A.
Variable One:A.
Variable neg:A->A.
Variable rec:A->A.   (*reciprocal 倒数*)

(* ################################################################# *)
(** * Generation of Zero Matrix *)

Section Matrix_o.

(** ** Functions of Zero List and Two-dimensional list *)

Section Zero_list_dlist.

(** *** list_o *)
(*构造一个长度为n的全0list*)
(** [Zero;Zero;...;Zero],of which the length is n. *)
Fixpoint list_o n :=
  match n with
  | O => List.nil
  | S n' => List.cons Zero (list_o n')
  end.

(** *** dlist_o *)
(*构造一个长度为n的全0二维list，高度是m，宽度是n*)
(** [[Zero;Zero;...;Zero];...[Zero;Zero;...;Zero]], of which the 
    height is m and the width is n. *)
Fixpoint dlist_o m n:=
  match m with
  | O => List.nil
  | S m' => List.cons (list_o n) (dlist_o m' n)
  end.
(*List.cons (list_o n) (dlist_o m' n)
(list_o n)代表构成长度为n的一维list
(dlist_o m' n)代表剩下m-1行矩阵
*)
End Zero_list_dlist.

(** ** Properties of Functions of Zero List and Two-dimensional List *)

Section Zero_list_dlist_lemma.
(** *** list_o_length *)
(* 验证list_o n产生的list长度是n *)
(* The length of the list generated by list_o n is n. *)
Lemma list_o_length : forall n ,
  length (list_o n) = n .
Proof.
  intros.
  induction n.
  - simpl. auto.
  - simpl. f_equal. auto.
Qed.

(** *** dlist_o_length *)
(* dlist_o_height m n产生的list高度是m *)
(** The height of the two-dimensional list generated by dlist_o is m. *)
Lemma dlist_o_height : forall m n ,
  length (dlist_o m n) = m.
Proof.
  intros.
  induction m.
  - simpl. auto.
  - simpl. f_equal. auto.
Qed.

(** *** dlist_o_width *)
(* dlist_o_width m n产生的list高度是m *)
(** The width of the two-dimensional list generated by dlist_o is n. *)
Lemma dlist_o_width : forall m n ,
   width (dlist_o m n) n.
Proof.
  intros.
  induction m.
  induction n.
  - simpl. auto.
  - simpl. auto.
  - induction n.
    + simpl. auto.
    + simpl. split. f_equal. apply list_o_length. auto.
Qed.



End Zero_list_dlist_lemma.

(** ** MO *)
(** Generate a zero matrix with height m and width n. *)
Definition MO m n :=
  let dl := dlist_o m n in
  mkMat A m n dl (dlist_o_height m n) (dlist_o_width m n).

End Matrix_o.

(** * Generation of Unit Matrix *)

Section Matrix_I.

(** ** Functions of Unit List and Two-dimensional List *)

Section One_list_dlist.

(** *** list_i *)
(* 产生一个，第i个元素是1，其余元素是0的list*)
(** Generate a list with the i-th element as One, the rest elements
    as Zero, and a length of n. *)
Fixpoint list_i n i :=
  match n,i with
  | O,_ =>List.nil
  | S n',O => List.cons Zero (list_i n' O)
  | S n',S O => List.cons One (list_i n' O)
  | S n', S i' => List.cons Zero (list_i n' i')
  end.


(** *** dlist_i' *)
(* dlist产生一个逐渐递增的1元素的二维list *)
(** This function helps to realize the unit matrix generating
    function. It generates a two-dimensional list of length n
    with decreasing position of One element. *)
Fixpoint dlist_i' m n i :=
  match m with
  | O => List.nil
  | S m' => List.cons (list_i n (S i)) (dlist_i' m' n (S i))
  end.
(*先在第一行的S i位置，放一个1
再在第二行的S S i位置，放一个1
...
*)
Lemma height_dlist_i' : forall m n i ,
  height (dlist_i' m n i) = m.
Proof.
  induction m.
  - simpl. auto.
  - simpl. intros. f_equal. auto.
Qed.



End One_list_dlist.

Section One_list_dlist_lemma.


(** *** list_i_length *)
(*验证了list_i n m产生的list的长度是n*)
(** list_i n m produces a list of length n. *)
Lemma length_list_i : forall m n ,
  length (list_i n m) = n.
Proof.
  induction m.
  induction n.
  - simpl. auto.
  - simpl. f_equal. auto.
  - induction n.
    + simpl. auto.
    + simpl. induction m. simpl. auto. simpl. auto.
Qed.

Lemma width_dlist_i':forall m n i, 
  width  (dlist_i' m n i) n.
Proof.
  induction m. simpl. auto.
  induction n. simpl. auto. 
  split. apply length_list_i. apply IHm.
Qed. 

End One_list_dlist_lemma.

(** ** MI *)
(** Generate an identity matrix with height and width n. *)
Definition MI n := 
let ma := dlist_i' n n 0 in
  mkMat A n n ma (height_dlist_i' n n 0) (width_dlist_i' n n 0).

End Matrix_I.

Section Matrix_fst.

(** *** list_v *)
(*构造一个长度为n的全是value的list*)
(** [v;v;...;v],of which the length is n. *)
Fixpoint list_v n (v : A):=
  match n with
  | O => List.nil
  | S n' => List.cons v (list_v n' v)
  end.

Lemma length_list_v_n : forall n v ,
  length (list_v n (v : A)) = n.
Proof.
  intros.
  induction n.
  - simpl. auto.
  - simpl. f_equal. auto.
Qed.

(** *** list_one_with_i *)
(*构造一个长度为n的全是value的list,仅仅传递一个i参数，没有其他不同*)
(** [v;v;...;v],of which the length is n. *)
Fixpoint list_one_with_i n (i : nat) (v : A):=
  match n with
  | O => List.nil
  | S n' => List.cons One (list_one_with_i n' i v)
  end.

Lemma length_list_one_with_i : forall n i v ,
  length (list_one_with_i n (i : nat) (v : A)) = n.
Proof.
  intros.
  induction n.
  - simpl. auto.
  - simpl. auto.
Qed.
(** *** list_i *)
(* 产生一个，第i个元素是v，其余元素是0的list*)

Fixpoint list_i_v n i (v : A):=
  match n,i with
  | O,_ =>List.nil
  | S n',O => List.cons Zero (list_i_v n' O v)
  | S n',S O => List.cons v (list_i_v n' O v)
  | S n', S i' => List.cons Zero (list_i_v n' i' v)
  end.


Lemma length_list_i_v : forall m n v ,
  length (list_i_v n (m : nat) (v : A)) = n.
Proof.
  induction m. induction n.
  - simpl. auto.
  - simpl.  f_equal. auto.
  - induction n.
    + simpl. auto.
    + simpl. induction m. simpl. auto. simpl. auto.
Qed.
  


(** *** list_i_v_j_one *)
(* 产生一个，第i个元素是v,第j个元素是One，其余元素是0的list*)

Fixpoint list_i_v_j_one n i j (v : A):=
  match n,i,j with
  | O,_,_ =>List.nil
  | S n',O,O => List.cons Zero (list_i_v_j_one n' O j v)
  | S n',S O,S j' => List.cons v (list_i_v_j_one n' O j v)
  | S n',S i',S O => List.cons One (list_i_v_j_one n' i' j v)
  | S n', _, _  => List.cons Zero (list_i_v_j_one n' O j v)
  end.

Lemma length_list_i_v_j_one : forall n i j v ,
  length (list_i_v_j_one n i j (v : A)) = n.
Proof.
  induction n. simpl. auto.
  induction i. 
  induction j.
  - simpl. auto.
  - simpl. auto.
  - induction j. simpl. induction i. simpl. auto. simpl. auto.
  simpl. induction i. simpl. auto. induction j. simpl. auto. simpl. auto.
    
Qed.

(** *** dlist_1 *)
(* dlist产生一个逐渐递增的1元素的二维list *)
(* j i控制v的行数列数 *)

Fixpoint dlist_1 m n i j (v : A):=
  match m,j with
  | O,_ => List.nil
  | S m',O    => List.cons (list_i n (S i)) (dlist_1 m' n (S i) O v)
  | S m',S O  => List.cons (list_i_v_j_one n j (S i) v) (dlist_1 m' n (S i) O v)
  | S m',S j' => List.cons (list_i n (S i)) (dlist_1 m' n (S i) j' v)
  end.


Lemma height_dlist_1 : forall m n i j v,
  height (dlist_1 m n i j (v : A)) = m.
Proof.
  induction m.
  - simpl. auto.
  - simpl. induction j. simpl. auto.
  induction j. simpl. auto. 
  simpl. auto.
Qed.

Lemma width_dlist_1 : forall m n i j v,
  width  (dlist_1 m n i j (v : A)) n.
Proof.
  induction m. simpl. auto.
  induction n. simpl.
  induction j.
  - simpl. auto.
  - induction j. 
    simpl. auto. 
    simpl. auto.
  - simpl. 
  induction j. 
  induction i. 
    simpl. split. 
    f_equal. 
    apply length_list_i. auto.
    simpl. 
    split. f_equal. apply length_list_i. auto.

  induction j. 
  simpl. split. f_equal. apply length_list_i_v_j_one. auto.

  induction i. simpl. split. f_equal. apply length_list_i. auto.

  simpl. split. f_equal. apply length_list_i. auto.
Qed. 



(* list_one_with_i *)
(** *** list_i *)
(* 产生一个，第i个元素是v，其余元素是0的list*)

(** *** dlist_2 *)
(* dlist产生一个逐渐递增的1元素的二维list *)
(* x y控制需要交换的两行 ,但是x<y，比如1,3行互换，则x=1，y=3*)


(*

Fixpoint dlist_2 m n i x y:=
  match m,x,y with
  | O,_,_ => List.nil
  | S m',S x',S y' => List.cons (list_i n (S i)) (dlist_2 m' n (S i) x' y')
  | S m',S O ,S y' => List.cons (list_i n (i+y)) (dlist_2 m' n (S i) O y')
  | S m',_   ,S O  => List.cons (list_i n (i+x)) (dlist_2 m' n (S i) O O)
  | S m',O   , O   => List.cons (list_i n (S i)) (dlist_2 m' n (S i) O O)
  end.
(* 使用的时候，需要x<y,但是没法在程序中体现出来，目前还存在问题 *)

*)

(** *** dlist_3 *)
(* j控制行数 i控制列数 v是value *)

Fixpoint dlist_3 m n i j (v : A):=
  match m,j with
  | O,_ => List.nil
  | S m',O    => List.cons (list_i n (S i)) (dlist_3 m' n (S i) O v)
  | S m',S O  => List.cons (list_i_v n (S i) v) (dlist_3 m' n (S i) O v)
  | S m',S j' => List.cons (list_i n (S i)) (dlist_3 m' n (S i) j' v)
  end.


Lemma height_dlist_3 : forall m n i j v,
  height (dlist_3 m n i j (v : A)) = m.
Proof.
  induction m.
  - simpl. auto.
  - simpl. induction j. simpl. auto.
  induction j. simpl. auto. 
  simpl. auto.
Qed.  


Lemma width_dlist_3 : forall m n i j v,
  width  (dlist_3 m n i j (v : A)) n.
Proof.
  induction m. simpl. auto.
  induction n. simpl. induction j. simpl. auto. induction j. simpl. auto. simpl. auto.
  
  simpl. induction j.
  - induction i. simpl. split. f_equal. apply length_list_i. auto.
    simpl. split. f_equal. apply length_list_i. auto.
  - induction j. induction i. simpl. split. f_equal. apply length_list_i_v. auto.
    simpl. split. f_equal. apply length_list_i_v. auto.
    induction i. simpl. split. f_equal. apply length_list_i. auto.
    simpl. split. f_equal. apply length_list_i. auto.
Qed.

Definition MFST1 n i j (v : A):= 
let ma := dlist_1 n n i j (v : A) in
  mkMat A n n ma (height_dlist_1 n n i j (v : A)) (width_dlist_1 n n i j (v : A)).


Definition MFST3 n i j (v : A):= 
let ma := dlist_3 n n i j (v : A) in
  mkMat A n n ma (height_dlist_3 n n i j (v : A)) (width_dlist_3 n n i j (v : A)).


End Matrix_fst.


Section Matrix_inverse.

(* -v *)

Fixpoint dlist_1_inverse m n i j (v : A):=
  match m,j with
  | O,_ => List.nil
  | S m',O    => List.cons (list_i n (S i)) (dlist_1_inverse m' n (S i) O v)
  | S m',S O  => List.cons (list_i_v_j_one n j (S i) (neg v) ) (dlist_1_inverse m' n (S i) O v)
  | S m',S j' => List.cons (list_i n (S i)) (dlist_1_inverse m' n (S i) j' v)
  end.

(* 1/v *)

Fixpoint dlist_3_inverse m n i j (v : A):=
  match m,j with
  | O,_ => List.nil
  | S m',O    => List.cons (list_i n (S i)) (dlist_3_inverse m' n (S i) O v)
  | S m',S O  => List.cons (list_i_v n (S i) (rec v) ) (dlist_3_inverse m' n (S i) O v)
  | S m',S j' => List.cons (list_i n (S i)) (dlist_3_inverse m' n (S i) j' v)
  end.

Lemma height_dlist_1_inverse : forall m n i j v,
  height (dlist_1_inverse m n i j (v : A)) = m.
Proof.
  induction m.
  - simpl. auto.
  - simpl. induction j. simpl. auto.
  induction j. simpl. auto. 
  simpl. auto.
Qed.

Lemma width_dlist_1_inverse : forall m n i j v,
  width  (dlist_1 m n i j (v : A)) n.
Proof.
  induction m. simpl. auto.
  induction n. simpl.
  induction j.
  - simpl. auto.
  - induction j. simpl. auto. simpl. auto.
  - simpl. induction j. induction i. simpl. split. f_equal. apply length_list_i. auto.
  simpl. split. f_equal. apply length_list_i. auto.

  induction j. simpl. split. f_equal. apply length_list_i_v_j_one. auto.

  induction i. simpl. split. f_equal. apply length_list_i. auto.

  simpl. split. f_equal. apply length_list_i. auto.
Qed. 


Lemma height_dlist_3_inverse : forall m n i j v,
  height (dlist_3_inverse m n i j (v : A)) = m.
Proof.
  induction m.
  - simpl. auto.
  - simpl. induction j. simpl. auto.
  induction j. simpl. auto. 
  simpl. auto.
Qed.  


Lemma width_dlist_3_inverse : forall m n i j v,
  width  (dlist_3_inverse m n i j (v : A)) n.
Proof.
  induction m. simpl. auto.
  induction n. simpl. induction j. simpl. auto. induction j. simpl. auto. simpl. auto.
  
  simpl. induction j.
  - induction i. simpl. split. f_equal. apply length_list_i. auto.
    simpl. split. f_equal. apply length_list_i. auto.
  - induction j. induction i. simpl. split. f_equal. apply length_list_i_v. auto.
    simpl. split. f_equal. apply length_list_i_v. auto.
    induction i. simpl. split. f_equal. apply length_list_i. auto.
    simpl. split. f_equal. apply length_list_i. auto.
Qed.


End Matrix_inverse.

End Matrix_FST.

Require Import Reals.
Open Scope R.
Import ListNotations.
Section test.
  (* 规模3*3，i从0开始 *)
  Definition tm1:= dlist_3 R 0 1 3%nat 3%nat 0%nat 1%nat 3.
  Definition tm2:= [[3;0;0];[0;1;0];[0;0;1]].

Lemma eq1: tm1= tm2.
  Proof. unfold tm1,tm2. unfold dlist_3,list_i,list_i_v.
  simpl. auto.
  Qed.
End test.


